FDL - Step of Proof: assert_of

Step of Proof: assert_of_bnot

9,38

Inference at * 1
Iof proof for Lemma assert of bnot:

1. p :

(

p))

(

p))

by ((((BoolInd 1)

CollapseTHEN (((Unfolds ``assert bnot not`` 0)

CollapseTHEN (Rewrite (

CRepeatC (HigherC ifthenelse_evalC)) 0))

))

)

CollapseTHEN ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

Definitions ff, if b then t else f fi , tt, t T, A, b, b, P Q, False, Unit, , ,

Lemmas true wf, false wf

Definitions	ff, if b then t else f fi , tt, t T, A, b, b, P Q, False, Unit, , ,
Lemmas	true wf, false wf